Library circumcircle

Require Export PointsType.
Require Import PointsETC.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition is_on_circumcircle P :=
 match P with cTriple x y z ⇒
  a×y×z + b×z×x + c×x×y = 0
 end.

Lemma is_on_circumcircle_ok :
 is_on_circumcircle pointA ∧ is_on_circumcircle pointB ∧ is_on_circumcircle pointC.
Proof.
intros.
unfold is_on_circumcircle.
simpl.
repeat split;ring.
Qed.

Lemma X_74_is_on_circumcenter :
 is_on_circumcircle X_74.
Proof.
intros.
red;simpl.
unfold SA,SB,SC;repeat split;field.
Qed.

End Triangle.